lemmas 11,40
STM: m-sys-at-feasible

STM: m-sys-at wf2

origin